Background: we have 2 separate installs of jedit tailored for 2 different workfows
(multi-user). Attempting to merge them using '-settings=/some/where/else' command-line
switch:
dmaziuk@stingray:~$ java -Xmx96m -Xms24m -jar /share/java/jEdit/5.0.0/jedit.jar -noserver
-settings=/share/java/jEdit/mrannotator/
12:56:25 PM [main] [error] main: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/activity.log
(Permission denied)
After making that a+w:
PluginJAR: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/jars-cache/QuickNotepad.jar.summary
(No such file or directory)
and
IOUtilities: Error moving file: java.io.FileNotFoundException: /share/java/jEdit/mrannotator/properties
(Is a directory) : /share/java/jEdit/mrannotator/properties (Is a directory)
12:57:18 PM [AWT-EventQueue-0] [error] jEdit: Failed to rename "/share/java/jEdit/mrannotator/#properties#save#"
to the user properties file "/share/java/jEdit/mrannotator/properties"
So clearly '-settings' overrides "user.home/.jedit" -- why have it in the first place
when I can just 'java -Duser.home=/some/place/else' ?
Or should I file a feature request for (e.g.) '-global-settings=' switch instead ?
| Submitted | dmaziuk - 2013-01-07 - 19:14:45z | Assigned | nobody |
|---|---|---|---|
| Priority | 5 | Category | None |
| Status | Open | Group | None |
| Resolution | None | Visibility | No |
| 2013-01-07 - 19:33:55z ezust |
You are getting permission denied messages because of permissions problems, and you're
trying to use a shared area for settings that are used by multiple users at the same
time? It is possible to put some site properties in the jedit home directory, if you want to share settings between multiple users, but a user settings directory must be owned by that user and only used by one user at a time. What platform is this? http://www.jedit.org/users-guide/settings-directory.html Site Properties You may also put properties files in the "properties" directory in the jEdit home directory (NOT the .jedit settings directory). You can locate the jEdit home directory by going to the Utilities menu directory, then the "jEdit Home Directory" menu item, and the first item in the pullout menu will be the location of the jEdit home directory. This is intended for site-wide settings and it is useful for things like a set of custom key bindings that you might want to share between different computers. This lets you keep your custom properties separate from the jEdit properties, so they are easier to find, edit, and move between machines. Note that your custom properties files must have ".props" as the file name extension. Site properties files are read in alphabetically by file name. This means that if you have a property with the same name in more than one file, the value for that property will be the value found in the last file that was read. You can edit these files inside jEdit - changes made to these files will not be re-read until the next time jEdit is started. |
|---|---|
| 2013-01-07 - 19:58:10z dmaziuk |
What I'd like is to share a set of modes, macros, and plugins between different *users*.
Specifically, a user working on file type X today will have the macros and modes for
X. Tomorrow they'll work on file type Y and have the plugins and modes for that. I guess on second thought it'd take both '-global-plugins/-global-modes/-global-macros' for what I want and properties for plugin toolbar & docking settings... assuming the user's properties add to the "site" ones -- the README doesn't look like they do. The platform is linux and yes, I am familiar with unix permissions and I know what the error messages mean. |
| 2013-01-07 - 20:59:32z ezust |
So you want an additional sharable user settings directory? Moving to feature requests. |
| 2013-01-07 - 21:09:52z ezust |
There is a shared set of modes, macros and plugins in jEdit's home directory. You
can customize different jEdit installations that way. What is the harm of having jedit.jar
and documentation there too? Also, that error message I see in the original ticket seems to indicate that a directory called "properties" is being opened as a file and failing. perhaps you should rmdir that folder and let jEdit create a properties file. |
| 2013-01-07 - 22:22:04z dmaziuk |
So the two currently available options is to have 2 separate jEdit installs & remeber
to upgrade it ttwwiiccee, or have all plugins, macros, and modes available to everyone
through the menus -- but use custom '-settings' to turn on and off the relevant UI
elements. I think #2 works as long as there's no filename conflicts in the plugins and modes. I also realised it's moot because we can't run our custom code on 5.x without updating it (cleaning up BufferChangeListeners and who knows what else) and that's not happening anytime soon. And if you do get a featuire in, it's not getting added to 4.2 (that we run), so it'll be of little use to me. So anyway, an option tro read plugins/modes/macros from a different global directory may be worth having, or maybe not. |